Search Results

Documents authored by Bjørner, Nikolaj

Document
DOI: 10.4230/LIPIcs.SAT.2022.26
Analysis of Core-Guided MaxSat Using Cores and Correction Sets

Authors: Nina Narodytska and Nikolaj Bjørner

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
Core-guided solvers are among the best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution at each relaxation step. In addition, the relaxations allow generating a large set of minimal cores (MUSes) of the original formula. However, properties of these cores in relation to the optimization objective have not been investigated. In contrast, minimum hitting set based solvers (MaxHS) extract a set of cores that are known to have properties related to the optimization objective, e.g., the size of the minimum hitting set of the discovered cores equals the optimum when the solver terminates. In this work we analyze minimal cores and minimum correction sets (MinCSes) of the input formula and its sub-formulas that core-guided solvers produce. We demonstrate that a set of MUSes that a core-guided algorithm discovers possess the same key properties as cores extracted by MaxHS solvers. For instance, we prove the size of a minimum hitting set of these cores equals the optimal cost. We also show that it discovers all MinCSes of special subformulas of the input formula. We discuss theoretical and practical implications of our results.
Cite as

Nina Narodytska and Nikolaj Bjørner. Analysis of Core-Guided MaxSat Using Cores and Correction Sets. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{narodytska_et_al:LIPIcs.SAT.2022.26,
  author =	{Narodytska, Nina and Bj{\o}rner, Nikolaj},
  title =	{{Analysis of Core-Guided MaxSat Using Cores and Correction Sets}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.26},
  URN =		{urn:nbn:de:0030-drops-167006},
  doi =		{10.4230/LIPIcs.SAT.2022.26},
  annote =	{Keywords: maximum satisfiability, unsatisfiable cores, correction sets}
}
Document
DOI: 10.4230/DagRep.9.2.27
Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)

Authors: Sébastien Bardin, Nikolaj Bjørner, and Cristian Cadar

Published in: Dagstuhl Reports, Volume 9, Issue 2 (2019)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 19062 "Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving", whose main goals were to bring together leading researchers in the different subfields of automated reasoning and constraint solving, foster greater communication between these communities and exchange ideas about new research directions. Constraint solving is at the heart of several key technologies, including program analysis, testing, formal methods, compilers, security analysis, optimization, and AI. During the last two decades, constraint solving has been highly successful and transformative: on the one hand, SAT/SMT solvers have seen a significant performance improvement with a concomitant impact on software engineering, formal methods and security; on the other hand, CP solvers have also seen a dramatic performance improvement, with deep impact in AI and optimization. These successes bring new applications together with new challenges, not yet met by any current technology. The seminar brought together researchers from SAT, SMT and CP along with application researchers in order to foster cross-fertilization of ideas, deepen interactions, identify the best ways to serve the application fields and in turn help improve the solvers for specific domains.
Cite as

Sébastien Bardin, Nikolaj Bjørner, and Cristian Cadar. Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062). In Dagstuhl Reports, Volume 9, Issue 2, pp. 27-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{bardin_et_al:DagRep.9.2.27,
  author =	{Bardin, S\'{e}bastien and Bj{\o}rner, Nikolaj and Cadar, Cristian},
  title =	{{Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)}},
  pages =	{27--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{2},
  editor =	{Bardin, S\'{e}bastien and Bj{\o}rner, Nikolaj and Cadar, Cristian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.2.27},
  URN =		{urn:nbn:de:0030-drops-108574},
  doi =		{10.4230/DagRep.9.2.27},
  annote =	{Keywords: Automated Decision Procedures, Constraint Programming, SAT, SMT}
}
Document
DOI: 10.4230/LIPIcs.ICLP.2011.73
Canonical Regular Types

Authors: Ethan K. Jackson, Nikolaj Bjørner, and Wolfram Schulte

Published in: LIPIcs, Volume 11, Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) (2011)

Abstract
Regular types represent sets of structured data, and have been used in logic programming (LP) for verification. However, first-class regular type systems are uncommon in LP languages. In this paper we present a new approach to regular types, based on type canonization, aimed at providing a practical first-class regular type system.
Cite as

Ethan K. Jackson, Nikolaj Bjørner, and Wolfram Schulte. Canonical Regular Types. In Technical Communications of the 27th International Conference on Logic Programming (ICLP'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 11, pp. 73-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ICLP.2011.73,
  author =	{Jackson, Ethan K. and Bj{\o}rner, Nikolaj and Schulte, Wolfram},
  title =	{{Canonical Regular Types}},
  booktitle =	{Technical Communications of the 27th International Conference on Logic Programming (ICLP'11)},
  pages =	{73--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-31-6},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{11},
  editor =	{Gallagher, John P. and Gelfond, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2011.73},
  URN =		{urn:nbn:de:0030-drops-31806},
  doi =		{10.4230/LIPIcs.ICLP.2011.73},
  annote =	{Keywords: Regular types, Canonical forms, Type canonizer}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact